feat: do not export private declarations #8337

Kha · 2025-05-14T16:11:58Z

This PR adjusts the experimental module system to not export any private declarations from modules.

Fixes #5002

Kha · 2025-05-14T16:12:08Z

!bench

leanprover-community-bot · 2025-05-14T16:46:14Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-8337 build failed against this PR. (2025-05-14 16:46:13) View Log
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f214708636a0ac8240ced8d0b0829614ad5c7f2b --onto 3af9ab64ed79a667fb8989f7a0c258b018aba371. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-28 14:24:54)
Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f214708636a0ac8240ced8d0b0829614ad5c7f2b --onto 921ce7682e46544b536b3ab2901233b06c8165cf. (2025-05-29 12:34:14)

leanprover-bot · 2025-05-14T17:06:11Z

Here are the benchmark results for commit 58edbda.
There were significant changes against commit 29cc755:

  Benchmark                   Metric                 Change
  ====================================================================
+ Init size                   bytes .olean            -9.1%
- Init size                   bytes .olean.private     4.8%
+ bv_decide_inequality.lean   task-clock              -6.2%  (-21.5 σ)
+ bv_decide_inequality.lean   wall-clock              -5.9%  (-24.0 σ)
+ import Lean                 branches                -3.3%  (-89.9 σ)
+ import Lean                 instructions            -3.6%  (-89.3 σ)
+ import Lean                 maxrss                  -1.3%  (-77.5 σ)
+ import Lean                 task-clock             -10.9%  (-25.8 σ)
+ import Lean                 wall-clock             -10.9%  (-25.3 σ)
+ lake build clean            instructions            -1.1%  (-23.9 σ)
+ lake build clean            task-clock              -4.7%  (-43.0 σ)
+ lake build clean            wall-clock              -3.6%  (-21.7 σ)
+ lake config elab            instructions            -1.2%  (-76.1 σ)
+ lake config elab            maxrss                  -1.2%  (-29.2 σ)
+ lake config import          instructions            -2.5% (-192.3 σ)
+ lake config import          maxrss                  -2.5% (-143.3 σ)
+ lake config tree            instructions            -2.4%  (-34.8 σ)
+ lake config tree            maxrss                  -2.5%  (-47.9 σ)
+ lake env                    instructions            -2.5% (-124.2 σ)
+ lake env                    maxrss                  -2.5%  (-72.8 σ)
+ language server startup     branches                -1.3%  (-36.2 σ)
+ language server startup     instructions            -1.4%  (-32.5 σ)
- nat_repr                    branches                 1.4%  (247.0 σ)
- nat_repr                    instructions             1.4%  (194.8 σ)
+ stdlib                      maxrss                  -1.6% (-172.3 σ)
+ stdlib                      wall-clock              -2.5%  (-37.1 σ)
- stdlib size                 bytes .olean.private     4.8%
+ workspaceSymbols            maxrss                  -1.6%  (-25.2 σ)

src/Init/Core.lean

Kha · 2025-05-16T09:47:22Z

!bench

leanprover-bot · 2025-05-16T10:41:21Z

Here are the benchmark results for commit 6886d98.
There were significant changes against commit 528fe0b:

  Benchmark     Metric                 Change
  ===========================================
+ Init size     bytes .olean.private    -2.4%
+ stdlib size   bytes .olean.private    -2.4%

Kha · 2025-05-28T13:52:08Z

src/Lean/Environment.lean

+  -- Private definitions are not exported but may still have relevant IR for other modules.
+  -- TODO: restrict to relevant defs that are `meta`/inlining-relevant/...
+  if env.setExporting true |>.contains name then


@zwarich My "use the private name encoding to find the source module of an IR decl" idea did not work out because of specalization names, so now we're using extraConstNames for them, for now.

Should we just change the specialization name encoding?

I don't think it matters until we start restricting the data of declMapExt itself

nomeata

Seems plausible

nomeata · 2025-05-28T14:21:09Z

src/Lean/Elab/SyntheticMVars.lean

+            let mut e ← instantiateExprMVars (.mvar mvarId')
+            if !e.isFVar then
+              e ← mvarId'.withContext do
+                AbstractNestedProofs.visit.mkAuxLemma e |>.run { cache := true } |>.run


This looks like it’s using “internal” functions from AbstractNestedProofs? Why not Lean.Meta.abstractNestedProofs?

Thanks for the reminder, I did want to refactor this before I forgot

src/Lean/Elab/SyntheticMVars.lean

Kha · 2025-05-28T16:15:53Z

!bench

leanprover-bot · 2025-05-28T16:43:14Z

Here are the benchmark results for commit 3fe3eeb.
There were significant changes against commit f214708:

  Benchmark        Metric                 Change
  =========================================================
+ Init size        bytes .olean.private    -3.3%
- bv_decide_mul    wall-clock               1.8%   (74.1 σ)
- qsort            instructions             5.3% (1028.0 σ)
- riscv-ast.lean   branches                 3.7%   (39.1 σ)
- riscv-ast.lean   instructions             3.5%   (34.1 σ)
- stdlib           blocked                  1.5%   (34.0 σ)
+ stdlib size      bytes .olean.private    -3.3%

leanprover-community-bot · 2025-05-30T21:48:29Z

✅ Mathlib branch lean-pr-testing-8337 has successfully built against this PR. (2025-05-30 21:48:27) View Log

* Update lean-toolchain for testing leanprover/lean4#8347 * fixes for leanprover/lean4#8347 * Update lean-toolchain for testing leanprover/lean4#8397 * deprecations for leanprover/lean4#8397 * chore: bump to nightly-2025-05-19 * chore: adaptations for nightly-2025-05-19 * Trigger CI for leanprover/lean4#8347 * Update the style linter to use LinterOptions * Fix test * chore: adaptations for nightly-2025-05-19 (#25017) Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Anne C.A. Baanen <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> * chore: bump to nightly-2025-05-20 * Merge master into nightly-testing * feat: a `grind` test case (#25037) Adds a test case for `grind` that was previously failing in the presence of Mathlib's typeclass shortcuts. Let's just keep it in Mathlib as a regression test. Note that this is a PR to `bump/v4.21.0`, as it requires a recent nightly toolchain. (It can still be reviewed and bors'd as any other PR.) * lake update * fixes * fixes * fixes * fixes * fix * fixes * fixes * shake --update * chore: bump to nightly-2025-05-21 * Update lean-toolchain for testing leanprover/lean4#7352 * lake update * Trigger CI for leanprover/lean4#7352 * chore: adaptations for nightly-2025-05-21 * chore: adaptations for nightly-2025-05-21 (#25079) Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Anne C.A. Baanen <[email protected]> * chore: adaptations for nightly-2025-05-21 * fix for leanprover/lean4#7352 * remove unneeded List.ofFn_succ from simp sets * Merge master into nightly-testing * Merge master into nightly-testing * Revert "fix for leanprover/lean4#7352" This reverts commit 38ca408. * chore: fix some defeq abuse in theorem statements around the `Id` monad (#25098) Follows on from leanprover/lean4#7352. This also deprecates: * `id.mk`, which looks like a porting error * `Free(Add)(Magma|Semigroup).mul_map_seq`, which is a garbage lemma that both is not meaningfully about the free objects and has defeq abuse everywhere. * chore: bump to nightly-2025-05-22 * update batteries * chore: bump to nightly-2025-05-23 * Update lean-toolchain for testing leanprover/lean4#8449 * chore: adaptations for nightly-2025-05-22 (#25110) Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: github-actions <[email protected]> * remove now upstreamed `clear_value` * Update lean-toolchain for testing leanprover/lean4#8457 * chore: update tests for `Format` bug fix * Trigger CI for leanprover/lean4#8457 * lake update * lake update * fixes * Merge master into nightly-testing * chore: bump to nightly-2025-05-24 * fix * chore: adaptations for nightly-2025-05-24 (#25147) Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: github-actions <[email protected]> * chore: adaptations for nightly-2025-05-24 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8470 * chore: bump to nightly-2025-05-25 * chore: adaptations for nightly-2025-05-25 * chore: adaptations for nightly-2025-05-25 (#25184) Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: github-actions <[email protected]> * unsimp `List.getElem?_length` This is solved using `getElem?_neg` now. * chore: adaptations for nightly-2025-05-25 * Trigger CI for leanprover/lean4#8470 * chore: bump to nightly-2025-05-26 * lake update * deprecations * Trigger CI for leanprover/lean4#8449 * Merge master into nightly-testing * chore: bump to nightly-2025-05-27 * chore: adaptations for nightly-2025-05-27 * Update lean-toolchain for testing leanprover/lean4#8504 * chore: bump to nightly-2025-05-28 * chore: adaptations for nightly-2025-05-27 (#25234) Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Kim Morrison <[email protected]> * fix * fix merge * fix merge again * deprecations * deprecations * fix Archive * comment out test * Fix and re-enable directory dependency lint test. * chore: bump to nightly-2025-05-29 * Use the formatting from the master branch. (Seems to have been a merge that went wrong.) * lake update * chore: adaptations for nightly-2025-05-28 (#25295) Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: github-actions <[email protected]> * fix * Trigger CI for leanprover/lean4#8337 * fixes * Merge master into nightly-testing * chore: bump to nightly-2025-05-30 * chore: adaptations for nightly-2025-05-29 (#25306) Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Rob23oba <[email protected]> * chore: bump to nightly-2025-05-31 * chore: bump to nightly-2025-06-01 * fix Archive * chore: adaptations for nightly-2025-06-01 (#25355) Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Anne C.A. Baanen <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> * chore: bump to nightly-2025-06-02 * chore: adaptations for nightly-2025-06-02 (#25360) Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Anne C.A. Baanen <[email protected]> Co-authored-by: github-actions <[email protected]> * Update lean-toolchain for testing leanprover/lean4#8584 * chore: adaptations for nightly-2025-06-02 * chore: bump to nightly-2025-06-03 * fix * fix * Update lean-toolchain for testing leanprover/lean4#8610 * fix * chore: bump to nightly-2025-06-04 * bump toolchain --------- Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Anne C.A. Baanen <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Joseph Rotella <[email protected]>

* chore: adaptations for nightly-2025-05-21 * fix for leanprover/lean4#7352 * remove unneeded List.ofFn_succ from simp sets * Merge master into nightly-testing * Merge master into nightly-testing * Revert "fix for leanprover/lean4#7352" This reverts commit 38ca408. * chore: fix some defeq abuse in theorem statements around the `Id` monad (#25098) Follows on from leanprover/lean4#7352. This also deprecates: * `id.mk`, which looks like a porting error * `Free(Add)(Magma|Semigroup).mul_map_seq`, which is a garbage lemma that both is not meaningfully about the free objects and has defeq abuse everywhere. * chore: bump to nightly-2025-05-22 * update batteries * chore: bump to nightly-2025-05-23 * Update lean-toolchain for testing leanprover/lean4#8449 * chore: adaptations for nightly-2025-05-22 (#25110) Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: github-actions <[email protected]> * remove now upstreamed `clear_value` * Update lean-toolchain for testing leanprover/lean4#8457 * chore: update tests for `Format` bug fix * Trigger CI for leanprover/lean4#8457 * lake update * lake update * fixes * Merge master into nightly-testing * chore: bump to nightly-2025-05-24 * fix * chore: adaptations for nightly-2025-05-24 (#25147) Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: github-actions <[email protected]> * chore: adaptations for nightly-2025-05-24 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8470 * chore: bump to nightly-2025-05-25 * chore: adaptations for nightly-2025-05-25 * chore: adaptations for nightly-2025-05-25 (#25184) Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: github-actions <[email protected]> * unsimp `List.getElem?_length` This is solved using `getElem?_neg` now. * chore: adaptations for nightly-2025-05-25 * Trigger CI for leanprover/lean4#8470 * chore: bump to nightly-2025-05-26 * lake update * deprecations * Trigger CI for leanprover/lean4#8449 * Merge master into nightly-testing * chore: bump to nightly-2025-05-27 * chore: adaptations for nightly-2025-05-27 * Update lean-toolchain for testing leanprover/lean4#8504 * chore: bump to nightly-2025-05-28 * chore: adaptations for nightly-2025-05-27 (#25234) Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Kim Morrison <[email protected]> * fix * Update lean-toolchain for testing leanprover/lean4#8519 * fix merge * fix merge again * deprecations * deprecations * fix Archive * comment out test * Fix and re-enable directory dependency lint test. * chore: bump to nightly-2025-05-29 * Use the formatting from the master branch. (Seems to have been a merge that went wrong.) * lake update * chore: adaptations for nightly-2025-05-28 (#25295) Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: github-actions <[email protected]> * fix * Trigger CI for leanprover/lean4#8337 * Trigger CI for leanprover/lean4#8519 * fixes * Merge master into nightly-testing * chore: bump to nightly-2025-05-30 * chore: adaptations for nightly-2025-05-29 (#25306) Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Rob23oba <[email protected]> * chore: bump to nightly-2025-05-31 * chore: bump to nightly-2025-06-01 * chore: remove simp attribute when value of argument can not be inferred by simp * fix Archive * chore: adaptations for nightly-2025-06-01 (#25355) Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Anne C.A. Baanen <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> * chore: bump to nightly-2025-06-02 * chore: adaptations for nightly-2025-06-02 (#25360) Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: Anne C.A. Baanen <[email protected]> Co-authored-by: github-actions <[email protected]> * Update lean-toolchain for testing leanprover/lean4#8584 * chore: adaptations for nightly-2025-06-02 * change phrasing of comments * chore(Geometry/Manifold): two simp-lemmas can be proven by simp * fix two lint problems * Trigger CI for leanprover/lean4#8519 * chore: bump to nightly-2025-06-03 * fix * fix * Update lean-toolchain for testing leanprover/lean4#8610 * fix * revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * cleanup lakefile --------- Co-authored-by: mathlib4-bot <[email protected]> Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Kim Morrison <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Rob23oba <[email protected]> Co-authored-by: Joseph Rotella <[email protected]> Co-authored-by: Anne C.A. Baanen <[email protected]> Co-authored-by: Sebastian Ullrich <[email protected]> Co-authored-by: Johan Commelin <[email protected]> Co-authored-by: Jovan Gerbscheid <[email protected]> Co-authored-by: Joachim Breitner <[email protected]>

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label May 14, 2025

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 14, 2025

Update lean-toolchain for testing leanprover/lean4#8337

cc8c2f9

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 14, 2025

Update lean-toolchain for testing leanprover/lean4#8337

e439229

leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label May 14, 2025

Rob23oba reviewed May 14, 2025

View reviewed changes

src/Init/Core.lean Show resolved Hide resolved

Kha force-pushed the push-yrmrrukrkmkq branch 5 times, most recently from 2f371ff to 6886d98 Compare May 16, 2025 09:45

Kha force-pushed the push-yrmrrukrkmkq branch 4 times, most recently from 86ee842 to c7702ad Compare May 28, 2025 12:52

Kha marked this pull request as ready for review May 28, 2025 12:58

Kha requested review from digama0, kim-em, leodemoura and zwarich as code owners May 28, 2025 12:58

Kha added the changelog-language Language features, tactics, and metaprograms label May 28, 2025

Kha commented May 28, 2025

View reviewed changes

nomeata approved these changes May 28, 2025

View reviewed changes

Kha force-pushed the push-yrmrrukrkmkq branch from a6f24e2 to 3fe3eeb Compare May 28, 2025 15:42

Kha added 13 commits May 30, 2025 17:44

fix: public accesses to private defs

4b3f1e0

chore: workaround for Meta.Closure failure

ed47c36

chore: other adaptions

b59c7f8

chore: fix tests

473c73b

chore: fix stage2

7ea6f97

chore: refactor use of AbstractNestedProofs.mkAuxLemma

38a4069

fix: do not run tactics with metavariables

b566a74

chore: adapt to by mvars restriction

acad052

perf: inline private_decl%s

de50df5

feat: number of imported constants in --stats

3e02108

fix: eval should adhere to stderrAsMessages

397e51f

fix: access to private definitions in the language server

40c8b5a

chore: add test

f1146d6

Kha force-pushed the push-yrmrrukrkmkq branch 2 times, most recently from f60bbd3 to 658d85a Compare May 30, 2025 16:11

Kha added 2 commits May 30, 2025 22:31

minor

cacd18b

fix: back compat

ba2ff62

Kha force-pushed the push-yrmrrukrkmkq branch from 658d85a to ba2ff62 Compare May 30, 2025 20:32

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 30, 2025

Trigger CI for leanprover/lean4#8337

f98c8cb

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 30, 2025

Trigger CI for leanprover/lean4#8337

cc32576

Kha added this pull request to the merge queue Jun 2, 2025

Merged via the queue into leanprover:master with commit 569e460 Jun 2, 2025
22 of 23 checks passed

Kha deleted the push-yrmrrukrkmkq branch June 2, 2025 08:54

feat: do not export private declarations #8337

feat: do not export private declarations #8337

Uh oh!

Conversation

Kha commented May 14, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Kha commented May 14, 2025

Uh oh!

leanprover-community-bot commented May 14, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented May 14, 2025

Uh oh!

Uh oh!

Kha commented May 16, 2025

Uh oh!

leanprover-bot commented May 16, 2025

Uh oh!

Kha May 28, 2025

Choose a reason for hiding this comment

Uh oh!

zwarich May 28, 2025

Choose a reason for hiding this comment

Uh oh!

Kha May 28, 2025

Choose a reason for hiding this comment

Uh oh!

nomeata left a comment

Choose a reason for hiding this comment

Uh oh!

nomeata May 28, 2025

Choose a reason for hiding this comment

Uh oh!

Kha May 28, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Kha commented May 28, 2025

Uh oh!

leanprover-bot commented May 28, 2025

Uh oh!

leanprover-community-bot commented May 30, 2025

Uh oh!

Uh oh!

Uh oh!

Kha commented May 14, 2025 •

edited

Loading

leanprover-community-bot commented May 14, 2025 •

edited

Loading